{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "from pyeda.inter import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "DIGITS = \"123456789\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "X = exprvars('x', (1, 10), (1, 10), (1, 10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "V = And(*[\n",
    "        And(*[\n",
    "            OneHot(*[X[r,c,v] for v in range(1, 10)])\n",
    "                     for c in range(1, 10)]\n",
    "        )\n",
    "        for r in range(1, 10)]\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "R = And(*[\n",
    "        And(*[\n",
    "            OneHot(*[X[r,c,v] for c in range(1, 10)])\n",
    "                     for v in range(1, 10)]\n",
    "        )\n",
    "        for r in range(1, 10)]\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "C = And(*[\n",
    "        And(*[\n",
    "            OneHot(*[X[r,c,v] for r in range(1, 10)])\n",
    "                     for v in range(1, 10)]\n",
    "        )\n",
    "        for c in range(1, 10)]\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "B = And(*[\n",
    "        And(*[\n",
    "            OneHot(*[\n",
    "                X[3*br+r,3*bc+c,v]\n",
    "                    for r in range(1, 4)\n",
    "                    for c in range(1, 4)]\n",
    "            )\n",
    "            for v in range(1, 10)]\n",
    "        )\n",
    "        for br in range(3) for bc in range(3)]\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "S = And(V, R, C, B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "len(S.xs)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "# This step does absorption\n",
    "S = S.to_cnf()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "len(S.xs)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def parse_grid(grid):\n",
    "    chars = [c for c in grid if c in DIGITS or c in \"0.\"]\n",
    "    assert len(chars) == 9 ** 2\n",
    "    return And(*[ X[i // 9 + 1, i % 9 + 1, int(c)]\n",
    "                  for i, c in enumerate(chars) if c in DIGITS ])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "grid = ( \".73|...|8..\"\n",
    "         \"..4|13.|.5.\"\n",
    "         \".85|..6|31.\"\n",
    "         \"---+---+---\"\n",
    "         \"5..|.9.|.3.\"\n",
    "         \"..8|.1.|5..\"\n",
    "         \".1.|.6.|..7\"\n",
    "         \"---+---+---\"\n",
    "         \".51|6..|28.\"\n",
    "         \".4.|.52|9..\"\n",
    "         \"..2|...|64.\" )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def get_val(point, r, c):\n",
    "    for v in range(1, 10):\n",
    "        if point[X[r,c,v]]:\n",
    "            return DIGITS[v-1]\n",
    "    return \"X\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def display(point):\n",
    "    chars = list()\n",
    "    for r in range(1, 10):\n",
    "        for c in range(1, 10):\n",
    "            if c in (4, 7):\n",
    "                chars.append(\"|\")\n",
    "            chars.append(get_val(point, r, c))\n",
    "        if r != 9:\n",
    "            chars.append(\"\\n\")\n",
    "            if r in (3, 6):\n",
    "                chars.append(\"---+---+---\\n\")\n",
    "    print(\"\".join(chars))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def solve(grid):\n",
    "    with parse_grid(grid):\n",
    "        return S.satisfy_one()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "display(solve(grid))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.4.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}
